|
| 1: |
|
app'(app'(eq,0),0) |
→ true |
| 2: |
|
app'(app'(eq,0),app'(s,x)) |
→ false |
| 3: |
|
app'(app'(eq,app'(s,x)),0) |
→ false |
| 4: |
|
app'(app'(eq,app'(s,x)),app'(s,y)) |
→ app'(app'(eq,x),y) |
| 5: |
|
app'(app'(le,0),y) |
→ true |
| 6: |
|
app'(app'(le,app'(s,x)),0) |
→ false |
| 7: |
|
app'(app'(le,app'(s,x)),app'(s,y)) |
→ app'(app'(le,x),y) |
| 8: |
|
app'(app'(app,nil),y) |
→ y |
| 9: |
|
app'(app'(app,app'(app'(add,n),x)),y) |
→ app'(app'(add,n),app'(app'(app,x),y)) |
| 10: |
|
app'(min,app'(app'(add,n),nil)) |
→ n |
| 11: |
|
app'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ app'(app'(if_min,app'(app'(le,n),m)),app'(app'(add,n),app'(app'(add,m),x))) |
| 12: |
|
app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) |
→ app'(min,app'(app'(add,n),x)) |
| 13: |
|
app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) |
→ app'(min,app'(app'(add,m),x)) |
| 14: |
|
app'(app'(rm,n),nil) |
→ nil |
| 15: |
|
app'(app'(rm,n),app'(app'(add,m),x)) |
→ app'(app'(app'(if_rm,app'(app'(eq,n),m)),n),app'(app'(add,m),x)) |
| 16: |
|
app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) |
→ app'(app'(rm,n),x) |
| 17: |
|
app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ app'(app'(add,m),app'(app'(rm,n),x)) |
| 18: |
|
app'(app'(minsort,nil),nil) |
→ nil |
| 19: |
|
app'(app'(minsort,app'(app'(add,n),x)),y) |
→ app'(app'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)),y) |
| 20: |
|
app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ app'(app'(add,n),app'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil)) |
| 21: |
|
app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ app'(app'(minsort,x),app'(app'(add,n),y)) |
|
There are 40 dependency pairs:
|
| 22: |
|
APP'(app'(eq,app'(s,x)),app'(s,y)) |
→ APP'(app'(eq,x),y) |
| 23: |
|
APP'(app'(eq,app'(s,x)),app'(s,y)) |
→ APP'(eq,x) |
| 24: |
|
APP'(app'(le,app'(s,x)),app'(s,y)) |
→ APP'(app'(le,x),y) |
| 25: |
|
APP'(app'(le,app'(s,x)),app'(s,y)) |
→ APP'(le,x) |
| 26: |
|
APP'(app'(app,app'(app'(add,n),x)),y) |
→ APP'(app'(add,n),app'(app'(app,x),y)) |
| 27: |
|
APP'(app'(app,app'(app'(add,n),x)),y) |
→ APP'(app'(app,x),y) |
| 28: |
|
APP'(app'(app,app'(app'(add,n),x)),y) |
→ APP'(app,x) |
| 29: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(app'(if_min,app'(app'(le,n),m)),app'(app'(add,n),app'(app'(add,m),x))) |
| 30: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(if_min,app'(app'(le,n),m)) |
| 31: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(app'(le,n),m) |
| 32: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(le,n) |
| 33: |
|
APP'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(min,app'(app'(add,n),x)) |
| 34: |
|
APP'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(app'(add,n),x) |
| 35: |
|
APP'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(min,app'(app'(add,m),x)) |
| 36: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(app'(app'(if_rm,app'(app'(eq,n),m)),n),app'(app'(add,m),x)) |
| 37: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(app'(if_rm,app'(app'(eq,n),m)),n) |
| 38: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(if_rm,app'(app'(eq,n),m)) |
| 39: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(app'(eq,n),m) |
| 40: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(eq,n) |
| 41: |
|
APP'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) |
→ APP'(app'(rm,n),x) |
| 42: |
|
APP'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) |
→ APP'(rm,n) |
| 43: |
|
APP'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ APP'(app'(add,m),app'(app'(rm,n),x)) |
| 44: |
|
APP'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ APP'(app'(rm,n),x) |
| 45: |
|
APP'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ APP'(rm,n) |
| 46: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(app'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)),y) |
| 47: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)) |
| 48: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))) |
| 49: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(app'(eq,n),app'(min,app'(app'(add,n),x))) |
| 50: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(eq,n) |
| 51: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(min,app'(app'(add,n),x)) |
| 52: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(add,n),app'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil)) |
| 53: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil) |
| 54: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)) |
| 55: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(app,app'(app'(rm,n),x)),y) |
| 56: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app,app'(app'(rm,n),x)) |
| 57: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(rm,n),x) |
| 58: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(rm,n) |
| 59: |
|
APP'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ APP'(app'(minsort,x),app'(app'(add,n),y)) |
| 60: |
|
APP'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ APP'(minsort,x) |
| 61: |
|
APP'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ APP'(app'(add,n),y) |
|
The approximated dependency graph contains one SCC:
{22,24,27,29,31,33,35-37,39,41,44,46,47,49,51,53,55,57,59}.